0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 20 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇒, 45 ms)
↳8 QDP
↳9 QDPSizeChangeProof (⇔, 0 ms)
↳10 YES
ackerman_in_gga(0, N, s(N)) → ackerman_out_gga(0, N, s(N))
ackerman_in_gga(s(M), 0, Res) → U1_gga(M, Res, ackerman_in_gga(M, s(0), Res))
ackerman_in_gga(s(M), s(N), Res) → U2_gga(M, N, Res, ackerman_in_gga(s(M), N, Res1))
U2_gga(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → U3_gga(M, N, Res, ackerman_in_gga(M, Res1, Res))
U3_gga(M, N, Res, ackerman_out_gga(M, Res1, Res)) → ackerman_out_gga(s(M), s(N), Res)
U1_gga(M, Res, ackerman_out_gga(M, s(0), Res)) → ackerman_out_gga(s(M), 0, Res)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
ackerman_in_gga(0, N, s(N)) → ackerman_out_gga(0, N, s(N))
ackerman_in_gga(s(M), 0, Res) → U1_gga(M, Res, ackerman_in_gga(M, s(0), Res))
ackerman_in_gga(s(M), s(N), Res) → U2_gga(M, N, Res, ackerman_in_gga(s(M), N, Res1))
U2_gga(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → U3_gga(M, N, Res, ackerman_in_gga(M, Res1, Res))
U3_gga(M, N, Res, ackerman_out_gga(M, Res1, Res)) → ackerman_out_gga(s(M), s(N), Res)
U1_gga(M, Res, ackerman_out_gga(M, s(0), Res)) → ackerman_out_gga(s(M), 0, Res)
ACKERMAN_IN_GGA(s(M), 0, Res) → U1_GGA(M, Res, ackerman_in_gga(M, s(0), Res))
ACKERMAN_IN_GGA(s(M), 0, Res) → ACKERMAN_IN_GGA(M, s(0), Res)
ACKERMAN_IN_GGA(s(M), s(N), Res) → U2_GGA(M, N, Res, ackerman_in_gga(s(M), N, Res1))
ACKERMAN_IN_GGA(s(M), s(N), Res) → ACKERMAN_IN_GGA(s(M), N, Res1)
U2_GGA(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → U3_GGA(M, N, Res, ackerman_in_gga(M, Res1, Res))
U2_GGA(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → ACKERMAN_IN_GGA(M, Res1, Res)
ackerman_in_gga(0, N, s(N)) → ackerman_out_gga(0, N, s(N))
ackerman_in_gga(s(M), 0, Res) → U1_gga(M, Res, ackerman_in_gga(M, s(0), Res))
ackerman_in_gga(s(M), s(N), Res) → U2_gga(M, N, Res, ackerman_in_gga(s(M), N, Res1))
U2_gga(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → U3_gga(M, N, Res, ackerman_in_gga(M, Res1, Res))
U3_gga(M, N, Res, ackerman_out_gga(M, Res1, Res)) → ackerman_out_gga(s(M), s(N), Res)
U1_gga(M, Res, ackerman_out_gga(M, s(0), Res)) → ackerman_out_gga(s(M), 0, Res)
ACKERMAN_IN_GGA(s(M), 0, Res) → U1_GGA(M, Res, ackerman_in_gga(M, s(0), Res))
ACKERMAN_IN_GGA(s(M), 0, Res) → ACKERMAN_IN_GGA(M, s(0), Res)
ACKERMAN_IN_GGA(s(M), s(N), Res) → U2_GGA(M, N, Res, ackerman_in_gga(s(M), N, Res1))
ACKERMAN_IN_GGA(s(M), s(N), Res) → ACKERMAN_IN_GGA(s(M), N, Res1)
U2_GGA(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → U3_GGA(M, N, Res, ackerman_in_gga(M, Res1, Res))
U2_GGA(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → ACKERMAN_IN_GGA(M, Res1, Res)
ackerman_in_gga(0, N, s(N)) → ackerman_out_gga(0, N, s(N))
ackerman_in_gga(s(M), 0, Res) → U1_gga(M, Res, ackerman_in_gga(M, s(0), Res))
ackerman_in_gga(s(M), s(N), Res) → U2_gga(M, N, Res, ackerman_in_gga(s(M), N, Res1))
U2_gga(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → U3_gga(M, N, Res, ackerman_in_gga(M, Res1, Res))
U3_gga(M, N, Res, ackerman_out_gga(M, Res1, Res)) → ackerman_out_gga(s(M), s(N), Res)
U1_gga(M, Res, ackerman_out_gga(M, s(0), Res)) → ackerman_out_gga(s(M), 0, Res)
ACKERMAN_IN_GGA(s(M), 0, Res) → ACKERMAN_IN_GGA(M, s(0), Res)
ACKERMAN_IN_GGA(s(M), s(N), Res) → U2_GGA(M, N, Res, ackerman_in_gga(s(M), N, Res1))
U2_GGA(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → ACKERMAN_IN_GGA(M, Res1, Res)
ACKERMAN_IN_GGA(s(M), s(N), Res) → ACKERMAN_IN_GGA(s(M), N, Res1)
ackerman_in_gga(0, N, s(N)) → ackerman_out_gga(0, N, s(N))
ackerman_in_gga(s(M), 0, Res) → U1_gga(M, Res, ackerman_in_gga(M, s(0), Res))
ackerman_in_gga(s(M), s(N), Res) → U2_gga(M, N, Res, ackerman_in_gga(s(M), N, Res1))
U2_gga(M, N, Res, ackerman_out_gga(s(M), N, Res1)) → U3_gga(M, N, Res, ackerman_in_gga(M, Res1, Res))
U3_gga(M, N, Res, ackerman_out_gga(M, Res1, Res)) → ackerman_out_gga(s(M), s(N), Res)
U1_gga(M, Res, ackerman_out_gga(M, s(0), Res)) → ackerman_out_gga(s(M), 0, Res)
ACKERMAN_IN_GGA(s(M), 0) → ACKERMAN_IN_GGA(M, s(0))
ACKERMAN_IN_GGA(s(M), s(N)) → U2_GGA(M, ackerman_in_gga(s(M), N))
U2_GGA(M, ackerman_out_gga(Res1)) → ACKERMAN_IN_GGA(M, Res1)
ACKERMAN_IN_GGA(s(M), s(N)) → ACKERMAN_IN_GGA(s(M), N)
ackerman_in_gga(0, N) → ackerman_out_gga(s(N))
ackerman_in_gga(s(M), 0) → U1_gga(ackerman_in_gga(M, s(0)))
ackerman_in_gga(s(M), s(N)) → U2_gga(M, ackerman_in_gga(s(M), N))
U2_gga(M, ackerman_out_gga(Res1)) → U3_gga(ackerman_in_gga(M, Res1))
U3_gga(ackerman_out_gga(Res)) → ackerman_out_gga(Res)
U1_gga(ackerman_out_gga(Res)) → ackerman_out_gga(Res)
ackerman_in_gga(x0, x1)
U2_gga(x0, x1)
U3_gga(x0)
U1_gga(x0)
From the DPs we obtained the following set of size-change graphs: